YES 1.245
↳ HASKELL
↳ BR
((lookupFM :: FiniteMap Char a -> Char -> Maybe a) :: FiniteMap Char a -> Char -> Maybe a) |
import qualified Maybe import qualified Prelude |
||||||||||||||||||||||||
data FiniteMap a b = EmptyFM | Branch a b Int (FiniteMap a b) (FiniteMap a b) |
||||||||||||||||||||||||
instance (Eq a, Eq b) => Eq (FiniteMap a b) where |
||||||||||||||||||||||||
lookupFM :: Ord a => FiniteMap a b -> a -> Maybe b
|
import qualified FiniteMap import qualified Prelude |
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
((lookupFM :: FiniteMap Char a -> Char -> Maybe a) :: FiniteMap Char a -> Char -> Maybe a) |
import qualified Maybe import qualified Prelude |
||||||||||||||||||||||||
data FiniteMap b a = EmptyFM | Branch b a Int (FiniteMap b a) (FiniteMap b a) |
||||||||||||||||||||||||
instance (Eq a, Eq b) => Eq (FiniteMap a b) where |
||||||||||||||||||||||||
lookupFM :: Ord b => FiniteMap b a -> b -> Maybe a
|
import qualified FiniteMap import qualified Prelude |
lookupFM EmptyFM key = Nothing lookupFM (Branch key elt vw fm_l fm_r) key_to_find
| key_to_find < key
= lookupFM fm_l key_to_find | key_to_find > key
= lookupFM fm_r key_to_find | otherwise
= Just elt
lookupFM EmptyFM key = lookupFM4 EmptyFM key lookupFM (Branch key elt vw fm_l fm_r) key_to_find = lookupFM3 (Branch key elt vw fm_l fm_r) key_to_find
lookupFM1 key elt vw fm_l fm_r key_to_find True = lookupFM fm_r key_to_find lookupFM1 key elt vw fm_l fm_r key_to_find False = lookupFM0 key elt vw fm_l fm_r key_to_find otherwise
lookupFM0 key elt vw fm_l fm_r key_to_find True = Just elt
lookupFM2 key elt vw fm_l fm_r key_to_find True = lookupFM fm_l key_to_find lookupFM2 key elt vw fm_l fm_r key_to_find False = lookupFM1 key elt vw fm_l fm_r key_to_find (key_to_find > key)
lookupFM3 (Branch key elt vw fm_l fm_r) key_to_find = lookupFM2 key elt vw fm_l fm_r key_to_find (key_to_find < key)
lookupFM4 EmptyFM key = Nothing lookupFM4 wv ww = lookupFM3 wv ww
undefined
| False
= undefined
undefined = undefined1
undefined0 True = undefined
undefined1 = undefined0 False
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
(lookupFM :: FiniteMap Char a -> Char -> Maybe a) |
import qualified Maybe import qualified Prelude |
|||||||||
data FiniteMap a b = EmptyFM | Branch a b Int (FiniteMap a b) (FiniteMap a b) |
|||||||||
instance (Eq a, Eq b) => Eq (FiniteMap b a) where |
|||||||||
lookupFM :: Ord b => FiniteMap b a -> b -> Maybe a
|
|||||||||
|
|||||||||
|
|||||||||
|
|||||||||
|
|||||||||
|
import qualified FiniteMap import qualified Prelude |
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ QDP
↳ DependencyGraphProof
new_lookupFM2(wx26, wx27, wx28, wx29, wx30, wx31, Succ(wx320), Succ(wx330), h) → new_lookupFM2(wx26, wx27, wx28, wx29, wx30, wx31, wx320, wx330, h)
new_lookupFM2(wx26, wx27, wx28, wx29, wx30, wx31, Zero, Succ(wx330), h) → new_lookupFM(wx29, Char(Succ(wx31)), h)
new_lookupFM1(wx55, wx56, wx57, wx58, wx59, wx60, Succ(wx610), Succ(wx620), ba) → new_lookupFM1(wx55, wx56, wx57, wx58, wx59, wx60, wx610, wx620, ba)
new_lookupFM2(wx26, wx27, wx28, wx29, wx30, wx31, Zero, Zero, h) → new_lookupFM20(wx26, wx27, wx28, wx29, wx30, wx31, h)
new_lookupFM20(wx26, wx27, wx28, wx29, wx30, wx31, h) → new_lookupFM1(wx26, wx27, wx28, wx29, wx30, wx31, Succ(wx31), Succ(wx26), h)
new_lookupFM1(wx55, wx56, wx57, wx58, wx59, wx60, Succ(wx610), Zero, ba) → new_lookupFM(wx59, Char(Succ(wx60)), ba)
new_lookupFM(Branch(Char(Succ(wx3000)), wx31, wx32, wx33, wx34), Char(Zero), bb) → new_lookupFM(wx33, Char(Zero), bb)
new_lookupFM(Branch(Char(Zero), wx31, wx32, wx33, wx34), Char(Succ(wx400)), bb) → new_lookupFM(wx34, Char(Succ(wx400)), bb)
new_lookupFM2(wx26, wx27, wx28, wx29, wx30, wx31, Succ(wx320), Zero, h) → new_lookupFM1(wx26, wx27, wx28, wx29, wx30, wx31, Succ(wx31), Succ(wx26), h)
new_lookupFM(Branch(Char(Succ(wx3000)), wx31, wx32, wx33, wx34), Char(Succ(wx400)), bb) → new_lookupFM2(wx3000, wx31, wx32, wx33, wx34, wx400, wx400, wx3000, bb)
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
new_lookupFM(Branch(Char(Succ(wx3000)), wx31, wx32, wx33, wx34), Char(Zero), bb) → new_lookupFM(wx33, Char(Zero), bb)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
new_lookupFM1(wx55, wx56, wx57, wx58, wx59, wx60, Succ(wx610), Succ(wx620), ba) → new_lookupFM1(wx55, wx56, wx57, wx58, wx59, wx60, wx610, wx620, ba)
new_lookupFM2(wx26, wx27, wx28, wx29, wx30, wx31, Succ(wx320), Succ(wx330), h) → new_lookupFM2(wx26, wx27, wx28, wx29, wx30, wx31, wx320, wx330, h)
new_lookupFM2(wx26, wx27, wx28, wx29, wx30, wx31, Zero, Succ(wx330), h) → new_lookupFM(wx29, Char(Succ(wx31)), h)
new_lookupFM2(wx26, wx27, wx28, wx29, wx30, wx31, Zero, Zero, h) → new_lookupFM20(wx26, wx27, wx28, wx29, wx30, wx31, h)
new_lookupFM20(wx26, wx27, wx28, wx29, wx30, wx31, h) → new_lookupFM1(wx26, wx27, wx28, wx29, wx30, wx31, Succ(wx31), Succ(wx26), h)
new_lookupFM1(wx55, wx56, wx57, wx58, wx59, wx60, Succ(wx610), Zero, ba) → new_lookupFM(wx59, Char(Succ(wx60)), ba)
new_lookupFM(Branch(Char(Zero), wx31, wx32, wx33, wx34), Char(Succ(wx400)), bb) → new_lookupFM(wx34, Char(Succ(wx400)), bb)
new_lookupFM2(wx26, wx27, wx28, wx29, wx30, wx31, Succ(wx320), Zero, h) → new_lookupFM1(wx26, wx27, wx28, wx29, wx30, wx31, Succ(wx31), Succ(wx26), h)
new_lookupFM(Branch(Char(Succ(wx3000)), wx31, wx32, wx33, wx34), Char(Succ(wx400)), bb) → new_lookupFM2(wx3000, wx31, wx32, wx33, wx34, wx400, wx400, wx3000, bb)
From the DPs we obtained the following set of size-change graphs: